A:Type, eq:EqDecider(A), ds:fpf(A; x.Type), x:A.
subtype_rel(fpf-cap(ds; eq; x; void); fpf-cap(ds; eq; x; top)) 

latex

Definitions	x:A. B(x), fpf-cap(f; eq; x; z), top, if b then t else f fi , t  T, x. t(x), P  Q, tt, ff, prop{i:l}, , x(s), Unit, P  Q, P  Q,
Lemmas	fpf-dom wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, top wf, fpf wf, deq wf